﻿/************************************************************************
 * SMLib - State Model Library
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     SMLib\Storage\BDD.cs
 * Description  :     Implementation of BDD Structure: Used in model checking engine - MCGine
 * Change log   :     -2011:  Initial version
 * To Do        :
 ************************************************************************/

using System;
using System.Collections.Generic;
using System.Text;
using System.Threading;

//UniqueTable stores keys not nodes
namespace SMLib.Storage
{

    /// <summary>
    /// The Structure of Binary Decision Diagram
    /// </summary>
    public class BDD
    {
        /// <summary>
        /// The Structure of the Node of BDD
        /// </summary>
        /// <remarks>
        /// Variables are indexed from 1
        /// The variable index = 0 referes to the terminal node of True or False
        /// the variable with index = 1 is the highest level
        /// </remarks>
        public class BDDnode
        {
            public UInt64 refs = 0;
            
            /// <summary>
            /// Index of the Variable Name
            /// </summary>
            public int var;
            
            /// <summary>
            /// Index of the Left Successor for False Value
            /// </summary>
            public UInt64 succ0;
            
            /// <summary>
            /// Index of the Right Successor for True Value
            /// </summary>
            public UInt64 succ1;
            
            /// <summary>
            /// Cunstructor Method
            /// </summary>
            /// <param name="v">Variable Index</param>
            /// <param name="s0">Index of the Left Successor for False Value</param>
            /// <param name="s1">Index of the Right Successor for True Value</param>
            public BDDnode(int v, UInt64 s0, UInt64 s1)
            {
                var = v;
                succ0 = s0;
                succ1 = s1;
            }
            /// <summary>
            /// Cunstructor Method
            /// </summary>
            /// <param name="key">Input Key String</param>
            public BDDnode(string key)
            {
                string[] res = key.Split('.');
                var = Convert.ToInt32(res[0]);
                succ0 = Convert.ToUInt64(res[1]);
                succ1 = Convert.ToUInt64(res[2]);
                refs = Convert.ToUInt64(res[3]);
            }
            /// <summary>
            /// Is it a turminal Node?
            /// </summary>
            /// <returns>true if it is terminal node</returns>
            public bool IsTerminal()
            {
                //return (succ0 <= 1 && succ1 <= 1);
                return (var == 0);
            }
            /// <summary>
            /// Is it a turminal Node?
            /// </summary>
            /// <returns>true if it is terminal node</returns>
            public static bool IsTerminal(string key)
            {
                //return (succ0 <= 1 && succ1 <= 1);
                BDDnode temp = new BDDnode(key);
                return (temp.var == 0);
            }
            /// <summary>
            /// Is it TRUE value
            /// </summary>
            /// <returns>True if the value is constant true</returns>
            public bool GetVal()
            {
                return (succ1 == 1);
            }
            /// <summary>
            /// Get the Key string of the node
            /// </summary>
            /// <remarks>Key strings are used as index of hash tables</remarks>
            /// <returns>Key String in format of var.succ0.succ1</returns>
            public string GetKey()
            {
                return var.ToString() + "." + succ0.ToString() + "." + succ1.ToString() + "." + refs.ToString();
            }
            
            public string GetKeyShort()
            {
                string tempKey = GetKey();
                string[] str = tempKey.Split('.');
                return str[0] + "." + str[1] + "." + str[2];
            }
            
            public static string GetKeyShort(string tempKey)
            {
                string[] str = tempKey.Split('.');
                return str[0] + "." + str[1] + "." + str[2];
            }
            
            /// <summary>
            /// Get the Key string of the node
            /// </summary>
            /// <remarks>Key strings are used as index of hash tables</remarks>
            /// <returns>Key String in format of var.succ0.succ1</returns>
            /// <param name="var">variable index</param>
            /// <param name="succ0">index of successor0</param>
            /// <param name="succ1">index of successor1</param>
            public static string GetKey(int var, UInt64 succ0, UInt64 succ1,UInt64 refs)
            {
                return var.ToString() + "." + succ0.ToString() + "." + succ1.ToString() + "." + refs.ToString();
            }

        }

        #region "Garbage Collection"

        public UInt64 garbageCount = 1;
        public bool isGarbageCollected = false;
        protected bool saveGarbage = false;
        //protected void GarbageRemove()
        //{
        //    //string tempNode;
        //    //string tempKeyString;

        //    foreach (UInt64 tempKey in garbage.Keys)
        //    //for(int i = 0; i <= garbage.Keys.Count; i++)
        //    {
        //        if (uniqueTable.ContainsKey(tempKey))
        //        {
        //            //tempNode = uniqueTable[tempKey];
        //            ////tempKeyString = tempNode.GetKey();
        //            //uniqueTable.Remove(tempKey);
        //            //uniqueTableR.Remove(tempNode);
        //            //computedTable.Remove(tempNode);
        //            RemoveNode(tempKey);
        //            //!!! I can't remove the item in garbage table here
        //            if (interactive)
        //                Console.WriteLine("collect: " + tempKey);
        //        }
        //    }
        //    garbage.Clear();
        //    Console.WriteLine("Garbage Collection Applied.");
        //}
        /// <summary>
        /// Garbage Collection for a single Node
        /// </summary>
        /// <param name="node">The Node to be collected</param>
        //protected void GarbageCollectNode(UInt64 node)
        //{
        //    RemoveNode(node);
        //    //garbage.Remove(node);
        //    if (interactive)
        //        Console.WriteLine("Collect: " + node);
        //}
        /// <summary>
        /// Garbage Collection for a Path of Nodes
        /// </summary>
        /// <param name="root">The Root of the Path</param>
        protected void GarbageCollectPath(UInt64 root, bool enGarbageRoot)
        {
            BDDnode rootN = new BDDnode(uniqueTable[root]);
            if (rootN.var == 0) return;
            if (enGarbageRoot)
            {
                if (interactive)
                    Console.WriteLine("Path Collection on: " + root);
                DecRef(root);
                //if(!garbage.ContainsKey(root))
                //    EnGarbage(root);
            }
            //IncRef(root); //???????WHY
        }
        protected void IncRef(UInt64 index)
        {
            if (index == falseValue || index == trueValue) return;
            string oldKey = uniqueTable[index];
            BDDnode node = new BDDnode(oldKey);
            node.refs++;
            uniqueTable[index] = node.GetKey();
            if (interactive)
                Console.WriteLine("IncRef: " + index + "=" + node.refs);
            
        }
        protected void DecRef(UInt64 index)
        {
            if (index == falseValue || index == trueValue
                || new BDDnode(uniqueTable[index]).var == 1) //This line has been added in order to prevent a bug
                return;
            BDDnode node = new BDDnode(uniqueTable[index]);
            if (node.refs > 0)
            {
                node.refs--;
                uniqueTable[index] = node.GetKey();
            }
            if (node.refs == 0)
            {
                RemoveNode(index);
                if (interactive)
                    Console.WriteLine("Collect: " + index);
                DecRef(node.succ0);
                DecRef(node.succ1);
            }
        }

        #endregion

        #region "Switches
        /// <summary>
        /// Interactive mode
        /// </summary>
        public bool interactive = true;
        #endregion

        #region "Statistics"
        /// <summary>
        /// Number of levels added till now
        /// </summary>
        protected int levelCount = 0;
        /// <summary>
        /// number of nodes added till now
        /// </summary>
        protected UInt64 nodeCount = 0;
        #endregion

        #region "constants"
        /// <summary>
        /// Index for False Value
        /// </summary>
        public const UInt64 falseValue = 0;
        /// <summary>
        /// Index for True Value
        /// </summary>
        public const UInt64 trueValue = 1;
        #endregion

        #region "Dynamics"
        /// <summary>
        /// Forward hash from Node index to node structure
        /// </summary>
        protected Dictionary<UInt64, string> uniqueTable;
        /// <summary>
        /// Backward hash from Node structure to Node index
        /// </summary>
        protected Dictionary<string, UInt64> uniqueTableR;
        /// <summary>
        /// Temporary Hash
        /// </summary>
        protected Dictionary<string, UInt64> computedTable;
        #endregion

        /// <summary>
        /// Constructor
        /// </summary>
        public BDD()
        {
            uniqueTable = new Dictionary<UInt64, string>();
            uniqueTableR = new Dictionary<string, UInt64>();
            computedTable = new Dictionary<string, UInt64>();
            /*
             * intit    info    var     succ0   succ1
             * false    0       0       0       0
             * true     1       0       1       1
             * */
            BDDnode falseNode = new BDDnode(0, 0, 0);
            uniqueTable.Add(0, falseNode.GetKey());
            string tempKeyString = falseNode.GetKeyShort();
            uniqueTableR.Add(tempKeyString, 0);
            BDDnode trueNode = new BDDnode(0, 1, 1);
            uniqueTable.Add(1, trueNode.GetKey());
            tempKeyString = trueNode.GetKeyShort();
            uniqueTableR.Add(tempKeyString, 1);
            nodeCount = 2;
        }

        //  [CORRECT]
        protected void RemoveNode(UInt64 tempKey)
        {
            //BDDnode tempNode = uniqueTable[tempKey];
            string tempKeyString = uniqueTable[tempKey];// tempNode.GetKey();
            uniqueTable.Remove(tempKey);
            tempKeyString = BDDnode.GetKeyShort(tempKeyString);
            uniqueTableR.Remove(tempKeyString);
            computedTable.Remove(tempKeyString);    // !!!! Changes performance
            if (interactive)
                Console.WriteLine("remove: " + tempKey);
        }
        //  [CORRECT]
        public UInt64 ITE(UInt64 ifPart, UInt64 thenPart, UInt64 elsePart)
        {
            //Console.WriteLine("ITE\t" + ifPart.ToString() + "\t" + thenPart.ToString() + "\t" + elsePart.ToString());

            UInt64 result = 0;
            string tempKey = ifPart.ToString() + "." + thenPart.ToString() + "." + elsePart.ToString();
            //UInt64 tempValue;
            bool flag = false;
            if (computedTable.ContainsKey(tempKey))
            {
                result = computedTable[tempKey];
                if (uniqueTable.ContainsKey(result))
                    flag = true;
            }
            else
                flag = false;
            if(!flag)
            {
                BDDnode u = new BDDnode(uniqueTable[ifPart]);
                BDDnode v1 = new BDDnode(uniqueTable[thenPart]);
                BDDnode v2 = new BDDnode(uniqueTable[elsePart]);
                if (u.IsTerminal())
                    result = (u.GetVal() ? thenPart : elsePart);
                else
                {
                    int z = min(u.var, v1.var, v2.var);
                    UInt64 w1 = ITE(Cofactor(ifPart, z, true),
                                   Cofactor(thenPart, z, true),
                                   Cofactor(elsePart, z, true));
                    UInt64 w0 = ITE(Cofactor(ifPart, z, false),
                                   Cofactor(thenPart, z, false),
                                   Cofactor(elsePart, z, false));
                    UInt64 w;
                    //Elimination rule  !!!!!!!!!!!!!!!1
                    if (w0 == w1)
                        w = w1;
                    //Isomorphism rule
                    else
                    {
                        //  [DIFFERENT FROM MIT ALGORITHM]
                        bool b;
                        w = Find_Or_Add(z, w0, w1, out b);
                    }
                    //!!!! MEMORY OVERFLOW
                    try
                    {
                        computedTable.Add(tempKey, w);
                    }
                    catch //(Exception ex)
                    {
                        computedTable.Clear();
                    }
                    result = w;
                }
            }
            return result;
        }
        //  [CORRECT]
        /// <summary>
        /// Minimum order of variables
        /// </summary>
        /// <param name="u">First variable</param>
        /// <param name="v1">Second variable</param>
        /// <param name="v2">Third variable</param>
        /// <returns>The variable with the lowest order</returns>
        public int min(int u, int v1, int v2)
        {
            int tempMin = (u <= v1 ? u : v1);
            if (tempMin == 0) tempMin += (u + v1);
            if (tempMin > v2 && v2 != 0) tempMin = v2;
            return tempMin;
        }
        //  [CORRECT]
        public UInt64 Cofactor(UInt64 root, int variable, bool value)
        {
            UInt64 result;
            BDDnode v = new BDDnode(uniqueTable[root]);
            //  [CORRECT]
            if (v.IsTerminal())
                result = root;
            //  [ALMOST CORRECT]
            else
            {
                //  [CORRECT]
                //  [DIFFERENT FROM MIT ALGORITHM]
                //if (variable > v.var) //MINE
                if (variable < v.var)  //MIT
                    result = root; //MINE
                //result = Cofactor(root, variable, value); //MIT
                //  [CORRECT]
                ///* MINE
                else if (variable == v.var)
                    if (value)
                        result = v.succ1;
                    else
                        result = v.succ0;
                // * */
                //  [ALMOST CORRECT]
                else
                {
                    int z = v.var;
                    UInt64 w1 = Cofactor(v.succ1, variable, value);
                    UInt64 w0 = Cofactor(v.succ0, variable, value);
                    //  [NEEDS TEST]
                    if (w0 == w1)
                        result = w1;
                    //  [CORRECT]
                    else
                    {
                        bool b;
                        result = Find_Or_Add(z, w0, w1, out b);
                    }
                }
            }
//            if (interactive && false)
//            {
//                Console.WriteLine("COF(" + root.ToString() + "," + variable.ToString() + "," + value.ToString() + ") = " + result.ToString());
//                Console.ReadKey();
//            }
            return result;
        }
        //  [CORRECT]
        //public UInt64 Find_Or_Add(int variable, UInt64 succ0, UInt64 succ1)
        //{
        //    BDDnode tempNode = new BDDnode(variable, succ0, succ1);
        //    UInt64 id;
        //    if (!uniqueTableR.ContainsKey(tempNode.GetKey()))
        //    {
        //        id = nodeCount++;//uniqueTableR.Count;
        //        uniqueTable.Add(id, tempNode.GetKey());
        //        uniqueTableR.Add(tempNode.GetKey(), (UInt64)id);

        //        if (interactive)
        //        {
        //            Console.WriteLine("NODE:\t" + id.ToString() + "=" + variable.ToString() + "," + succ0.ToString() + "," + succ1.ToString());
        //            Console.ReadKey();
        //        }

        //        if (saveGarbage)
        //            if (!garbage.ContainsKey(id))
        //            {
        //                garbage.Add(id, true);
        //                if (interactive)
        //                    Console.WriteLine("garbage: " + id.ToString());
        //            }
        //    }
        //    else
        //    {
        //        id = uniqueTableR[tempNode.GetKey()];
        //        if (saveGarbage)
        //            garbage.Remove(id);
        //    }
        //    return id;
        //}
        public UInt64 Find_Or_Add(int variable, UInt64 succ0, UInt64 succ1, out bool found)
        {
            BDDnode tempNode = new BDDnode(variable, succ0, succ1);
            string tempKeyShort = tempNode.GetKeyShort();
            UInt64 id;
            if (!uniqueTableR.ContainsKey(tempKeyShort))
            {
                found = false;
                id = nodeCount++;//uniqueTableR.Count;
                uniqueTable.Add(id, tempNode.GetKey());
                uniqueTableR.Add(tempKeyShort, (UInt64)id);

                if (interactive)
                {
                    Console.WriteLine("NODE:\t" + id.ToString() + "=" + variable.ToString() + "," + succ0.ToString() + "," + succ1.ToString());
                    Console.ReadKey();
                }

                //if (saveGarbage)
                {
                    IncRef(succ0);
                    IncRef(succ1);
                }
            }
            else
            {
                found = true;
                id = uniqueTableR[tempKeyShort];
                //IncRef(id);
            }
            return id;
        }
        //  [CORRECT]
        public UInt64 Find_Or_Add(int variable)
        {
            bool b;
            return Find_Or_Add(variable, 0, 1, out b);
        }

        //  [ALMOST CORRECT]
        /// <summary>
        /// Existantial Quantification
        /// </summary>
        public UInt64 Existential(UInt64 root, int variable)
        {
            UInt64 z0 = Cofactor(root, variable, false);
            UInt64 z1 = Cofactor(root, variable, true);
            return ITE(z0, 1, z1);  //z0 or z1
        }
        //  [CORRECT]
        /// <summary>
        /// Existantial Quantification
        /// </summary>
        public UInt64 ExistentialVectorMid(UInt64 root)
        {
            int i = levelCount;
            UInt64 result = Existential(root, i);
            do
                result = Existential(result, i--);
            while (i > levelCount / 2);
            return result;
        }
        //  [CORRECT]
        /// <summary>
        /// Universal Quantification
        /// </summary>
        public UInt64 UniversalVectorMid(UInt64 root)
        {
            int i = levelCount;
            UInt64 result = Universal(root, i);
            do
                result = Universal(result, i--);
            while (i > levelCount / 2);
            return result;
        }

        //  [CORRECT]
        /// <summary>
        /// Universal Quantification
        /// </summary>
        public UInt64 Universal(UInt64 root, int variable)
        {
            UInt64 z0 = Cofactor(root, variable, false);
            UInt64 z1 = Cofactor(root, variable, true);
            return ITE(z0, z1, 0);  //z0 and z1
        }

        //  [CORRECT]
        /// <summary>
        /// Renames variables in a function
        /// </summary>
        /// <remarks>Variable numbers start from 1</remarks>
        /// <param name="root">Root Node</param>
        /// <param name="order">list of variable changes</param>
        /// <returns>A function with changed variables</returns>
        public UInt64 Rename(UInt64 root, Dictionary<int, int> order)
        {
            BDDnode v = new BDDnode(uniqueTable[root]);
            UInt64 w;
            int z;
            //  [CORRECT]
            if (v.IsTerminal())
                w = root;
            //  [CORRECT]
            else
            {
                UInt64 w0 = Rename(v.succ0, order);
                UInt64 w1 = Rename(v.succ1, order);
                if (order.ContainsKey(v.var))
                    z = order[v.var];
                else
                    z = v.var;
                bool b;
                w = Find_Or_Add(z, w0, w1, out b);//!!!!
            }
            return w;
        }
        //  [CORRECT]
        /// <summary>
        /// Renames variables in a function from x to x'
        /// </summary>
        /// <param name="root">Root Node</param>
        /// <returns>A function with changed variables</returns>
        public UInt64 Rename(UInt64 root)
        {
            Dictionary<int, int> order = new Dictionary<int, int>();
            for (int i = 0; i < levelCount / 2; i++)
                order[i + 1] = (i + 1) + (levelCount / 2);
            BDDnode v = new BDDnode(uniqueTable[root]);
            UInt64 w;
            int z;
            //  [CORRECT]
            if (v.IsTerminal())
                w = root;
            //  [CORRECT]
            else
            {
                UInt64 w0 = Rename(v.succ0, order);
                UInt64 w1 = Rename(v.succ1, order);
                if (order.ContainsKey(v.var))
                    z = order[v.var];
                else
                    z = v.var;
                bool b;
                w = Find_Or_Add(z, w0, w1, out b);//!!!!
            }
            return w;
        }
        //  [CORRECT]   [TestGen]
        public UInt64 GetSize()
        {
            return (UInt64) uniqueTable.Count;
        }
    }

    /// <summary>
    /// Provides High-level Methods for BDD
    /// </summary>
    public class myBDDex : BDD
    {
        //  [CORRECT]
        public UInt64 AND(UInt64 p, UInt64 q)
        {
            return ITE(p, q, falseValue);
        }
        //  [CORRECT]
        public UInt64 OR(UInt64 p, UInt64 q)
        {
            return ITE(p, trueValue, q);
        }
        /*
        //  [WRONG]   [Bitwise NOT]
        public UInt64 NOT(UInt64 p)
        {
            if (p == falseValue) return trueValue;
            if (p == trueValue) return falseValue;

            BDDnode tempNode = new BDDnode(uniqueTable[p]);
            bool b;
            //!this seems to have error
            //return Find_Or_Add(tempNode.var, tempNode.succ1, tempNode.succ0, out b);
            //this is wrong too!
            //return Find_Or_Add(tempNode.var, NOT(tempNode.succ1), NOT(tempNode.succ0), out b);
            UInt64 leftN = NOT(tempNode.succ0);
            UInt64 rightN = NOT(tempNode.succ1);

            if ((leftN == trueValue && rightN == falseValue) ||
               (rightN == trueValue && leftN == falseValue))
                return Find_Or_Add(tempNode.var, leftN, rightN, out b);
            if (rightN == trueValue)
                return Find_Or_Add(tempNode.var, falseValue, leftN, out b);
            if (leftN == trueValue)
                return Find_Or_Add(tempNode.var, rightN, falseValue, out b);
            return Find_Or_Add(tempNode.var, rightN, leftN, out b);
        }
         */
        //  [TEST]   
        public UInt64 NOT(UInt64 p)
        {
            if (p == falseValue) return trueValue;
            if (p == trueValue) return falseValue;

            BDDnode tempNode = new BDDnode(uniqueTable[p]);
            UInt64 leftN = NOT(tempNode.succ0);
            UInt64 rightN = NOT(tempNode.succ1);
            bool b;
            return Find_Or_Add(tempNode.var,leftN,rightN,out b);

        }
        //  [ENHANCE]   [TestGen]
        public UInt64 Add(bool[] seq)
        {

            bool found = false;
            UInt64 tempnode, tempnode2;
            int var = seq.Length;



            if (seq[var - 1])
                tempnode = Find_Or_Add(var, falseValue, trueValue, out found);
            else
                tempnode = Find_Or_Add(var, trueValue, falseValue, out found);


            var--;
            while (var > 0)
            {


                if (seq[var - 1])
                    tempnode2 = Find_Or_Add(var, falseValue, trueValue, out found);
                else
                    tempnode2 = Find_Or_Add(var, trueValue, falseValue, out found);




                tempnode = AND(tempnode, tempnode2);

                if (!found)
                    DecRef(tempnode2);

                var--;
            }
            if (seq.Length > levelCount) levelCount = seq.Length;
            


            return tempnode;
        }
        //  [ENHANCE]   [TestGen]
        public UInt64 Add(bool[] seq, UInt64 root)
        {
            //!!! mistake: the root is garbage not the tempNode
            //saveGarbage = isGarbageCollected;       //start garbage collector

            UInt64 tempNode = Add(seq);
            if (seq.Length > levelCount) levelCount = seq.Length;

            //!!! mistake: the root is garbage not the tempNode
            //saveGarbage = false;                    //stop garbage collector


            UInt64 res = OR(tempNode, root);


            if (root != 0)
            {
                //!!!! RACE CONDITION ON gargabe.keys
                //Thread th = new Thread(GarbageRemove);
                //th.Start();
                if(root!=res)
                    GarbageCollectPath(root, true);
                if(tempNode!=res)
                    GarbageCollectPath(tempNode, true);
                //GarbageRemove(tempNode);//?????????
            }

            return res;
        }
        //  [CORRECT]   [TestGen]
        public UInt64 Add(string seq)
        {
            bool[] vector = new bool[seq.Length];
            for (int i = 0; i < seq.Length; i++)
                vector[i] = (seq[i] == '1');
            UInt64 res = Add(vector);
            if (interactive)
                Console.WriteLine("added: " + seq + "\tRoot: " + res);
            return res;
        }
        //  [CORRECT]   [TestGen]
        public UInt64 Add(string seq, UInt64 root)
        {
            if (root == 0)
                return Add(seq);

            bool[] vector = new bool[seq.Length];
            for (int i = 0; i < seq.Length; i++)
                vector[i] = (seq[i] == '1');
            UInt64 res = Add(vector, root);
            if (interactive)
                Console.WriteLine("added: " + seq + "\tRoot: " + res);
            return res;
        }
        /*
        //  [CORRECT]   [TestGen]
        public bool Exists(bool[] seq, UInt64 root)
        {
            BDDnode node = new BDDnode(uniqueTable[root]);
            int var = node.var;

            do
            {
                if (node.var == 0)
                    return (node.succ0 == 1);
                if (seq[var - 1])
                    root = node.succ1;
                else
                    root = node.succ0;
                node = new BDDnode(uniqueTable[root]);
                var = node.var;
            } while (true);
        }
         */
        //  [CORRECT]   [TestGen]
        public bool Exists(string seq, UInt64 root)
        {
            BDDnode node = new BDDnode(uniqueTable[root]);
            int var = node.var;
            
            do
            {
                if (node.var == 0)
                    return (node.succ0 == 1);

                //Not Needed: ref to Note#1
                ////Added for case of variable length bitStrings
                //if (var > seq.Length)
                //    return false;

                if (var-1 >= seq.Length)
                    return false;
                if (seq[var - 1] == '1')
                    root = node.succ1;
                else
                    root = node.succ0;
                node = new BDDnode(uniqueTable[root]);
                var = node.var;
            } while (true);
        }

        //  [CORRECT]
        public void Trace(bool interactive)
        {
            Console.WriteLine("Info\tVar\tsucc0\tsucc1\t");
            BDDnode tempNode;
            foreach (UInt64 key in uniqueTable.Keys)
            {
                tempNode = new BDDnode(uniqueTable[key]);
                Console.WriteLine(key.ToString() + "|\t" + tempNode.var.ToString() + "\t" +
                                  tempNode.succ0.ToString() + "\t" + tempNode.succ1.ToString());
                if (interactive)
                    Console.ReadKey();
            }
            Console.ReadKey();
        }
        //  [CORRECT]
        public string Trace2String()
        {
            Console.WriteLine("Info\tVar\tsucc0\tsucc1\t");
            BDDnode tempNode;
            string temp = "";
            foreach (UInt64 key in uniqueTable.Keys)
            {
                tempNode = new BDDnode(uniqueTable[key]);
                temp += (key.ToString() + "|\t" + tempNode.var.ToString() + "\t" +
                                  tempNode.succ0.ToString() + "\t" + tempNode.succ1.ToString() + "\r\n");
            }
            return temp;
        }
        //  [CORRECT]
        public void Trace(UInt64 root)
        {
            BDDnode tempNode = new BDDnode(uniqueTable[root]);
            Console.WriteLine(root + "\t" + tempNode.succ0.ToString() + "\t" + tempNode.succ1.ToString());
            if (tempNode.var != 0)
            {
                Trace(tempNode.succ0);
                Trace(tempNode.succ1);
            }
        }
        //  [CORRECT]
        public string Trace2String(UInt64 root)
        {
            BDDnode tempNode = new BDDnode(uniqueTable[root]);
            string temp = "";
            if (tempNode.var != 0)
            {
                temp = (root + "\t" + tempNode.var.ToString() + "\t"  + tempNode.succ0.ToString() + "\t" + tempNode.succ1.ToString() + "\r\n");
                temp += Trace2String(tempNode.succ0);
                temp += Trace2String(tempNode.succ1);
            }
            return temp;
        }
        //  [CORRECT]
        public string TraceString(UInt64 root)
        {
            BDDnode tempNode = new BDDnode(uniqueTable[root]);
            string res = " ";
            //if (tempNode.var == 0)
            //{
            //    res = " " + tempNode.var.ToString();
            //    res += " (" + TraceString(tempNode.succ0);
            //    res += TraceString(tempNode.succ1) + " )";
            //}
            //else

            if (tempNode.var == 0)
                return " FALSE";
            //return (tempNode.succ0 == 1 ? " T" : " F");
            if (tempNode.succ0 == trueValue)
            {
                res += "~V" + tempNode.var.ToString();
                if (tempNode.succ1 != falseValue)
                {
                    res += " + V" + tempNode.var.ToString();
                    res += " (" + TraceString(tempNode.succ0);
                    res += " + " + TraceString(tempNode.succ1) + " )";
                }
            }
            else if (tempNode.succ1 == trueValue)
            {
                res += tempNode.var.ToString();
                if (tempNode.succ0 != falseValue)
                {
                    res += " + V" + tempNode.var.ToString();
                    res += " (" + TraceString(tempNode.succ0);
                    res += " + " + TraceString(tempNode.succ1) + " )";
                }
            }
            else
            {
                //??????????PROBLEM HERE
                res = " ~V" + tempNode.var.ToString();
                res += " (" + TraceString(tempNode.succ0) + " )";
                res += "+ V" + tempNode.var.ToString();
                res += " (" + TraceString(tempNode.succ1) + " )";
            }
            return res;
        }

        //  [CORRECT]
        public void ListStates(UInt64 root, List<string> list)
        {
            ListStates(root, list, "");
        }
        //  [CORRECT]
        private void ListStates(UInt64 root,List<string> list, string prefix)
        {
            string gap = "";
            BDDnode node = new BDDnode(uniqueTable[root]);
            if (root == trueValue)
            {
                for (int i = prefix.Length ; i < levelCount; i++)
                    gap += "X";
                list.Add(prefix + gap);
                return;
            }
            if(root == falseValue)
                return;
            
            for (int i = prefix.Length+1; i < node.var; i++)
                gap += "X";
            
            ListStates(node.succ0, list, prefix + gap + "0");
            ListStates(node.succ1, list, prefix + gap + "1");                       
        }
        //  [CORRECT]
        public string ListStatesString(UInt64 root)
        {
            List<string> list = new List<string>();
            ListStates(root, list);
            string res = "";
            foreach (string i in list)
                res += i + "\r\n";
            return res;
        }

    }
}